Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	active(f(X))	→ mark(cons(X,f(g(X))))
2:	active(g(0))	→ mark(s(0))
3:	active(g(s(X)))	→ mark(s(s(g(X))))
4:	active(sel(0,cons(X,Y)))	→ mark(X)
5:	active(sel(s(X),cons(Y,Z)))	→ mark(sel(X,Z))
6:	active(f(X))	→ f(active(X))
7:	active(cons(X1,X2))	→ cons(active(X1),X2)
8:	active(g(X))	→ g(active(X))
9:	active(s(X))	→ s(active(X))
10:	active(sel(X1,X2))	→ sel(active(X1),X2)
11:	active(sel(X1,X2))	→ sel(X1,active(X2))
12:	f(mark(X))	→ mark(f(X))
13:	cons(mark(X1),X2)	→ mark(cons(X1,X2))
14:	g(mark(X))	→ mark(g(X))
15:	s(mark(X))	→ mark(s(X))
16:	sel(mark(X1),X2)	→ mark(sel(X1,X2))
17:	sel(X1,mark(X2))	→ mark(sel(X1,X2))
18:	proper(f(X))	→ f(proper(X))
19:	proper(cons(X1,X2))	→ cons(proper(X1),proper(X2))
20:	proper(g(X))	→ g(proper(X))
21:	proper(0)	→ ok(0)
22:	proper(s(X))	→ s(proper(X))
23:	proper(sel(X1,X2))	→ sel(proper(X1),proper(X2))
24:	f(ok(X))	→ ok(f(X))
25:	cons(ok(X1),ok(X2))	→ ok(cons(X1,X2))
26:	g(ok(X))	→ ok(g(X))
27:	s(ok(X))	→ ok(s(X))
28:	sel(ok(X1),ok(X2))	→ ok(sel(X1,X2))
29:	top(mark(X))	→ top(proper(X))
30:	top(ok(X))	→ top(active(X))

There are 47 dependency pairs:


31:	ACTIVE(f(X))	→ CONS(X,f(g(X)))
32:	ACTIVE(f(X))	→ F(g(X))
33:	ACTIVE(f(X))	→ G(X)
34:	ACTIVE(g(0))	→ S(0)
35:	ACTIVE(g(s(X)))	→ S(s(g(X)))
36:	ACTIVE(g(s(X)))	→ S(g(X))
37:	ACTIVE(g(s(X)))	→ G(X)
38:	ACTIVE(sel(s(X),cons(Y,Z)))	→ SEL(X,Z)
39:	ACTIVE(f(X))	→ F(active(X))
40:	ACTIVE(f(X))	→ ACTIVE(X)
41:	ACTIVE(cons(X1,X2))	→ CONS(active(X1),X2)
42:	ACTIVE(cons(X1,X2))	→ ACTIVE(X1)
43:	ACTIVE(g(X))	→ G(active(X))
44:	ACTIVE(g(X))	→ ACTIVE(X)
45:	ACTIVE(s(X))	→ S(active(X))
46:	ACTIVE(s(X))	→ ACTIVE(X)
47:	ACTIVE(sel(X1,X2))	→ SEL(active(X1),X2)
48:	ACTIVE(sel(X1,X2))	→ ACTIVE(X1)
49:	ACTIVE(sel(X1,X2))	→ SEL(X1,active(X2))
50:	ACTIVE(sel(X1,X2))	→ ACTIVE(X2)
51:	F(mark(X))	→ F(X)
52:	CONS(mark(X1),X2)	→ CONS(X1,X2)
53:	G(mark(X))	→ G(X)
54:	S(mark(X))	→ S(X)
55:	SEL(mark(X1),X2)	→ SEL(X1,X2)
56:	SEL(X1,mark(X2))	→ SEL(X1,X2)
57:	PROPER(f(X))	→ F(proper(X))
58:	PROPER(f(X))	→ PROPER(X)
59:	PROPER(cons(X1,X2))	→ CONS(proper(X1),proper(X2))
60:	PROPER(cons(X1,X2))	→ PROPER(X1)
61:	PROPER(cons(X1,X2))	→ PROPER(X2)
62:	PROPER(g(X))	→ G(proper(X))
63:	PROPER(g(X))	→ PROPER(X)
64:	PROPER(s(X))	→ S(proper(X))
65:	PROPER(s(X))	→ PROPER(X)
66:	PROPER(sel(X1,X2))	→ SEL(proper(X1),proper(X2))
67:	PROPER(sel(X1,X2))	→ PROPER(X1)
68:	PROPER(sel(X1,X2))	→ PROPER(X2)
69:	F(ok(X))	→ F(X)
70:	CONS(ok(X1),ok(X2))	→ CONS(X1,X2)
71:	G(ok(X))	→ G(X)
72:	S(ok(X))	→ S(X)
73:	SEL(ok(X1),ok(X2))	→ SEL(X1,X2)
74:	TOP(mark(X))	→ TOP(proper(X))
75:	TOP(mark(X))	→ PROPER(X)
76:	TOP(ok(X))	→ TOP(active(X))
77:	TOP(ok(X))	→ ACTIVE(X)

The approximated dependency graph contains 8 SCCs: {52,70}, {51,69}, {53,71}, {54,72}, {55,56,73}, {58,60,61,63,65,67,68}, {40,42,44,46,48,50} and {74,76}.

Consider the SCC {52,70}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 52 is weakly decreasing and rule 70 is strictly decreasing. There is one new SCC.
- Consider the SCC {52}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 52 is strictly decreasing.

Consider the SCC {51,69}. There are no usable rules. By taking the AF π with π(F) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 51 is weakly decreasing and rule 69 is strictly decreasing. There is one new SCC.
- Consider the SCC {51}. By taking the AF π with π(F) = 1 together with the lexicographic path order with empty precedence, rule 51 is strictly decreasing.

Consider the SCC {53,71}. There are no usable rules. By taking the AF π with π(G) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 53 is weakly decreasing and rule 71 is strictly decreasing. There is one new SCC.
- Consider the SCC {53}. By taking the AF π with π(G) = 1 together with the lexicographic path order with empty precedence, rule 53 is strictly decreasing.

Consider the SCC {54,72}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 54 is weakly decreasing and rule 72 is strictly decreasing. There is one new SCC.
- Consider the SCC {54}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 54 is strictly decreasing.

Consider the SCC {55,56,73}. There are no usable rules. By taking the AF π with π(mark) = π(SEL) = 1 together with the lexicographic path order with empty precedence, the rules in {55,56} are weakly decreasing and rule 73 is strictly decreasing. There is one new SCC.
- Consider the SCC {55,56}. By taking the AF π with π(SEL) = 1 together with the lexicographic path order with empty precedence, rule 56 is weakly decreasing and rule 55 is strictly decreasing. There is one new SCC.
  - Consider the SCC {56}. By taking the AF π with π(SEL) = 2 together with the lexicographic path order with empty precedence, rule 56 is strictly decreasing.

Consider the SCC {58,60,61,63,65,67,68}. There are no usable rules. By taking the AF π with π(f) = π(g) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {58,63,65} are weakly decreasing and the rules in {60,61,67,68} are strictly decreasing. There is one new SCC.
- Consider the SCC {58,63,65}. By taking the AF π with π(f) = π(g) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {58,63} are weakly decreasing and rule 65 is strictly decreasing. There is one new SCC.
  - Consider the SCC {58,63}. By taking the AF π with π(f) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 58 is weakly decreasing and rule 63 is strictly decreasing. There is one new SCC.
    - Consider the SCC {58}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 58 is strictly decreasing.

Consider the SCC {40,42,44,46,48,50}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(cons) = π(f) = π(g) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {40,42,44,46} are weakly decreasing and the rules in {48,50} are strictly decreasing. There is one new SCC.
- Consider the SCC {40,42,44,46}. By taking the AF π with π(ACTIVE) = π(cons) = π(f) = π(g) = 1 together with the lexicographic path order with empty precedence, the rules in {40,42,44} are weakly decreasing and rule 46 is strictly decreasing. There is one new SCC.
  - Consider the SCC {40,42,44}. By taking the AF π with π(ACTIVE) = π(cons) = π(f) = 1 together with the lexicographic path order with empty precedence, the rules in {40,42} are weakly decreasing and rule 44 is strictly decreasing. There is one new SCC.
    - Consider the SCC {40,42}. By taking the AF π with π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, rule 42 is weakly decreasing and rule 40 is strictly decreasing. There is one new SCC.
      - Consider the SCC {42}. By taking the AF π with π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 42 is strictly decreasing.

Consider the SCC {74,76}. The usable rules are {1-28}. The constraints could not be solved.

Tyrolean Termination Tool (43.62 seconds) --- May 3, 2006